Skip to content

Conversation

@danakj
Copy link
Contributor

@danakj danakj commented Nov 18, 2025

Define rules for extend declarations (extend require and extend impl as) that say the facet type they name must be complete at the point of the declaration. Define completeness for a facet type to include all interfaces and named constraints that can be reached though extend require declarations.

@danakj danakj added proposal A proposal proposal draft Proposal in draft, not ready for review labels Nov 18, 2025
@danakj danakj force-pushed the proposal-extend-require branch from 5074db7 to cc668b4 Compare November 18, 2025 23:15
@danakj danakj force-pushed the proposal-extend-require branch from cc668b4 to 5e9d9ae Compare November 19, 2025 19:14
@danakj danakj marked this pull request as ready for review November 19, 2025 19:28
@danakj danakj requested review from a team as code owners November 19, 2025 19:28
@danakj danakj requested review from zygoloid and removed request for a team November 19, 2025 19:28
@danakj danakj changed the title Type completeness in extend require Type completeness in extend Nov 19, 2025
@github-actions github-actions bot added proposal rfc Proposal with request-for-comment sent out toolchain and removed proposal draft Proposal in draft, not ready for review labels Nov 19, 2025
@danakj danakj force-pushed the proposal-extend-require branch from 5e9d9ae to 16bdf5f Compare November 19, 2025 19:30
@danakj danakj force-pushed the proposal-extend-require branch from 16bdf5f to 7adc915 Compare November 19, 2025 19:31
Copy link
Contributor

@chandlerc chandlerc left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This generally LG on my end.

Copy link
Contributor Author

@danakj danakj left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

PTAL

@danakj danakj requested review from josh11b and zygoloid November 20, 2025 15:53
[#2760](https://github.com/carbon-language/carbon-lang/blob/trunk/proposals/p2760.md):
Consistent class and interface syntax

## Proposal
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Do we already have a rule for extend base and extend adapt declarations? If not, would it be worth adding them here too, so that we have complete coverage of all extend declarations?

Comment on lines +69 to +83
We call a `extend require` declaration _extend-reachable_ from a facet type if
it's enclosing interface or named constraint is part of that facet type, or if
its enclosing interface or named constraint is named by another
_extend-reachable_ declaration. That is, we can find a path from the facet type
to the `extend require` declaration through other `extend require` declarations.

We say that a facet type is complete if:

- All its _extend-reachable_ `extend require` declarations are complete. This
follows from the enclosing interface or named constraint being complete.
- We are able to form a specific for each interface and named constraint
extended by the facet type.
- We are able to form a specific for each _extend-reachable_ `extend require`
declaration in the context of the specific facet type being completed,
without monomorphization errors.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It'd be nice if we could say something broader here, and while I don't think we can avoid facet types being a special case, perhaps we can make them reuse the broader notion. What I'm thinking is something along the lines of:

"""
An extend declaration

extend base: X;
extend adapt X;
extend impl as X;
extend require impls X;

declares that the enclosing scope extends the scope associated with X. The extend declaration requires X to be complete, or, if X is a generic parameter, requires the type of X to be complete.

The scope of a facet type formed by a where declaration extends the scope of its first operand. The scope of a facet type formed by an & operator extends the scopes of both of its operands. In either case, the facet type is complete if every scope it extends is complete. The facet type type is associated with an empty scope and is complete.
"""

## Details

To `extend` an entity `Y` with another `Z` means that name lookups into `Y` will
also look into `Z`. At the end of the definition of `Y`, we expect to be able to
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I would expect this to apply immediately, not at the end of the definition of Y. For example:

base class Z {
   class X {}
}
class Y {
  extend base: Z;
  // Finds `X` in `Z`.
  fn F() -> X;
}

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment

Labels

proposal rfc Proposal with request-for-comment sent out proposal A proposal toolchain

Projects

None yet

Development

Successfully merging this pull request may close these issues.

4 participants